(declare-fun |main::i@3| () Int)
(declare-fun |main::i@4| () Int)
(declare-fun __POLICY_CHOICE_0 () Int)
(declare-fun |main::i@2| () Int)
(declare-fun __POLICY_CHOICE_2 () Int)
(declare-fun __POLICY_CHOICE_1 () Int)
(declare-fun |main::__CPAchecker_TMP_0@3| () Int)
(declare-fun __VERIFIER_nondet_bool@2 () Int)
(assert (let ((a!1 (or (and (not (<= |main::__CPAchecker_TMP_0@3| 0))
                    (= __POLICY_CHOICE_1 0))
               (and (not (>= |main::__CPAchecker_TMP_0@3| 0))
                    (= __POLICY_CHOICE_1 1))))
      (a!2 (or (and (not (<= |main::i@2| 4)) (= __POLICY_CHOICE_2 0))
               (and (not (>= |main::i@2| 4)) (= __POLICY_CHOICE_2 1)))))
  (and (or (and (= |main::__CPAchecker_TMP_0@3| __VERIFIER_nondet_bool@2)
                a!1
                (= |main::i@2| 4)
                (= |main::i@3| 0)
                (= __POLICY_CHOICE_0 0))
           (and (= |main::__CPAchecker_TMP_0@3| __VERIFIER_nondet_bool@2)
                a!1
                a!2
                (= |main::i@3| |main::i@2|)
                (= __POLICY_CHOICE_0 1)))
       (= |main::i@4| (+ 1 |main::i@3|)))))
(assert (let ((a!1 (= (- |main::i@2| 0) (* 2 (div (- |main::i@2| 0) 2)))))
  (and a!1 (<= |main::i@2| 0) (<= (* (- 1) |main::i@2|) 0))))
(assert (> |main::i@4| 0))
(maximize |main::i@4|)
(set-option :opt.optsmt_engine basic)
(set-option :opt.priority box)
(check-sat)
(get-objectives)
